Nuprl Lemma : implies-es-real 11,40
X:es_realizer{i:l}, P:(event_system{i:l}prop{i':l}).
R-Feasible{i:l}
R-Feasible(X)
 (es:event_system{i:l}. R-consistent(X; es)  P(es))
 es-real{i:l}
 es-real(es.P(es)) 
latex

Definitionst  T, P  Q, R-realizes{i:l}(R; es.P(es)), x:A. B(x), es-real{i:l}(es.P(es)), x(s), P  Q, prop{i:l}, x:A. B(x)
Lemmases realizer wf, event system wf, R-Feasible wf, R-consistent wf

origin